g:IMonoid, a, b:.
(a  b)
 (E:({a..b}|g|), k:. (*,e) a  j < b. E(j) = (*,e) a+k  j < b+k. E(j - k)  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	A, False, P  Q, {i..j}, |g|, x:AB(x), GrpSig, {x:A| B(x)} , A  B, x:A. B(x), Type, , t  T, IMonoid, P  Q, P & Q, P  Q, {T}, x.A(x), , s = t, *, e, (op,id) lb  i < ub. E(i), x. t(x), n+m, x(s), f(a), n - m, {i...}, x:A  B(x), i  j < k, x f y, T, True, -n, a < b
Lemmas	itop unroll hi, itop unroll base, int upper ind, int upper wf, itop wf, grp id wf, grp op wf, int le to int upper, imon wf, le wf, grp car wf, int seg wf